Mechanically Proving Termination Using Polynomial Interpretations
Identifieur interne : 005446 ( Main/Exploration ); précédent : 005445; suivant : 005447Mechanically Proving Termination Using Polynomial Interpretations
Auteurs : Evelyne Contejean [France] ; Claude Marché [France] ; Ana Paula Tomás [Portugal] ; Xavier Urbain [France]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2005-05-01.
English descriptors
Abstract
Abstract: For a long time, term orderings defined by polynomial interpretations were scarcely used in computer-aided termination proof of TRSs. But recently, the introduction of the dependency pairs approach achieved considerable progress w.r.t. automated termination proof, in particular by requiring from the underlying ordering much weaker properties than the classical approach. As a consequence, the noticeable power of a combination dependency pairs/polynomial orderings yielded a regain of interest for these interpretations. We describe criteria on polynomial interpretations for them to define weakly monotonic orderings. From these criteria, we obtain new techniques both for mechanically checking termination using a given polynomial interpretation and for finding such interpretations with full automation. With regard to automated search, we propose an original method for solving Diophantine constraints. We implemented these techniques into the CiME rewrite tool, and we provide some experimental results that show how useful polynomial orderings actually are in practice.
Url:
DOI: 10.1007/s10817-005-9022-x
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001374
- to stream Istex, to step Curation: 001357
- to stream Istex, to step Checkpoint: 001299
- to stream Main, to step Merge: 005592
- to stream Main, to step Curation: 005446
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Mechanically Proving Termination Using Polynomial Interpretations</title><author><name sortKey="Contejean, Evelyne" sort="Contejean, Evelyne" uniqKey="Contejean E" first="Evelyne" last="Contejean">Evelyne Contejean</name></author><author><name sortKey="Marche, Claude" sort="Marche, Claude" uniqKey="Marche C" first="Claude" last="Marché">Claude Marché</name></author><author><name sortKey="Tomas, Ana Paula" sort="Tomas, Ana Paula" uniqKey="Tomas A" first="Ana Paula" last="Tomás">Ana Paula Tomás</name></author><author><name sortKey="Urbain, Xavier" sort="Urbain, Xavier" uniqKey="Urbain X" first="Xavier" last="Urbain">Xavier Urbain</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5468F3F5B63A60CEA8EA7FFD86173D3E72C9CF18</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/s10817-005-9022-x</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-S66G069P-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001374</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001374</idno><idno type="wicri:Area/Istex/Curation">001357</idno><idno type="wicri:Area/Istex/Checkpoint">001299</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001299</idno><idno type="wicri:doubleKey">0168-7433:2006:Contejean E:mechanically:proving:termination</idno><idno type="wicri:Area/Main/Merge">005592</idno><idno type="wicri:Area/Main/Curation">005446</idno><idno type="wicri:Area/Main/Exploration">005446</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Mechanically Proving Termination Using Polynomial Interpretations</title><author><name sortKey="Contejean, Evelyne" sort="Contejean, Evelyne" uniqKey="Contejean E" first="Evelyne" last="Contejean">Evelyne Contejean</name><affiliation wicri:level="4"><country xml:lang="fr">France</country><wicri:regionArea>PCRI-LRI (CNRS UMR 8623) & INRIA Futurs Bât. 490, Université Paris-Sud, Centre d'Orsay, 91405, Orsay, Cedex</wicri:regionArea><orgName type="university">Université Paris-Sud</orgName><placeName><settlement type="city">Orsay</settlement><region type="region" nuts="2">Île-de-France</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Marche, Claude" sort="Marche, Claude" uniqKey="Marche C" first="Claude" last="Marché">Claude Marché</name><affiliation wicri:level="4"><country xml:lang="fr">France</country><wicri:regionArea>PCRI-LRI (CNRS UMR 8623) & INRIA Futurs Bât. 490, Université Paris-Sud, Centre d'Orsay, 91405, Orsay, Cedex</wicri:regionArea><orgName type="university">Université Paris-Sud</orgName><placeName><settlement type="city">Orsay</settlement><region type="region" nuts="2">Île-de-France</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Tomas, Ana Paula" sort="Tomas, Ana Paula" uniqKey="Tomas A" first="Ana Paula" last="Tomás">Ana Paula Tomás</name><affiliation wicri:level="1"><country xml:lang="fr">Portugal</country><wicri:regionArea>DCC-FC & LIACC, University of Porto, R. do Campo Alegre 823, 4150-180, Porto</wicri:regionArea><wicri:noRegion>Porto</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Portugal</country></affiliation></author><author><name sortKey="Urbain, Xavier" sort="Urbain, Xavier" uniqKey="Urbain X" first="Xavier" last="Urbain">Xavier Urbain</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>CEDRIC, IIE, Conservatoire National des Arts et Métiers, 18 allée Jean Rostand, 91025, Evry, Cedex</wicri:regionArea><wicri:noRegion>Cedex</wicri:noRegion><wicri:noRegion>Cedex</wicri:noRegion></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2005-05-01">2005-05-01</date><biblScope unit="volume">34</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="325">325</biblScope><biblScope unit="page" to="363">363</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>polynomial interpretations</term><term>term rewriting</term><term>termination</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: For a long time, term orderings defined by polynomial interpretations were scarcely used in computer-aided termination proof of TRSs. But recently, the introduction of the dependency pairs approach achieved considerable progress w.r.t. automated termination proof, in particular by requiring from the underlying ordering much weaker properties than the classical approach. As a consequence, the noticeable power of a combination dependency pairs/polynomial orderings yielded a regain of interest for these interpretations. We describe criteria on polynomial interpretations for them to define weakly monotonic orderings. From these criteria, we obtain new techniques both for mechanically checking termination using a given polynomial interpretation and for finding such interpretations with full automation. With regard to automated search, we propose an original method for solving Diophantine constraints. We implemented these techniques into the CiME rewrite tool, and we provide some experimental results that show how useful polynomial orderings actually are in practice.</div></front></TEI><affiliations><list><country><li>France</li><li>Portugal</li></country><region><li>Île-de-France</li></region><settlement><li>Orsay</li></settlement><orgName><li>Université Paris-Sud</li></orgName></list><tree><country name="France"><region name="Île-de-France"><name sortKey="Contejean, Evelyne" sort="Contejean, Evelyne" uniqKey="Contejean E" first="Evelyne" last="Contejean">Evelyne Contejean</name></region><name sortKey="Contejean, Evelyne" sort="Contejean, Evelyne" uniqKey="Contejean E" first="Evelyne" last="Contejean">Evelyne Contejean</name><name sortKey="Marche, Claude" sort="Marche, Claude" uniqKey="Marche C" first="Claude" last="Marché">Claude Marché</name><name sortKey="Marche, Claude" sort="Marche, Claude" uniqKey="Marche C" first="Claude" last="Marché">Claude Marché</name><name sortKey="Urbain, Xavier" sort="Urbain, Xavier" uniqKey="Urbain X" first="Xavier" last="Urbain">Xavier Urbain</name></country><country name="Portugal"><noRegion><name sortKey="Tomas, Ana Paula" sort="Tomas, Ana Paula" uniqKey="Tomas A" first="Ana Paula" last="Tomás">Ana Paula Tomás</name></noRegion><name sortKey="Tomas, Ana Paula" sort="Tomas, Ana Paula" uniqKey="Tomas A" first="Ana Paula" last="Tomás">Ana Paula Tomás</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005446 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005446 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:5468F3F5B63A60CEA8EA7FFD86173D3E72C9CF18
|texte= Mechanically Proving Termination Using Polynomial Interpretations
}}
| This area was generated with Dilib version V0.6.33. |  |